es:ES, L:(Id List).
fischer(L)
 (e1:E, j:Id.
 Newround(e1)  (j  L)  ((j = loc(e1)))  (the rcv(free message from e1 to j)  E)) 

latex

Definitions	if b then t else f fi , ff, eq_atom$n(x;y), Atom2Deq, IdDeq, t.1, eqof(d), , a = b, P  Q, b, P  Q, IdLnk, A c B, "$x", P & Q, the rcv(free message from e1 to j), t  T, A, Newround(e), P  Q, Id, x:A. B(x), False, xL. P(x), P  Q, @i(x:T), @e(xv), fischer(L)
Lemmas	event system wf, fischer wf, es-E wf, es-when wf, es-change-to wf, es-loc wf, Id wf, l member wf, not wf, false wf, assert-eq-id, eq id wf, assert wf, not functionality wrt iff, es-first-from wf